Nuprl Lemma : qadd_preserves_eq
11,40
postcript
pdf
a
,
b
,
c
:
. (
a
=
b
)
((
c
+
a
) = (
c
+
b
)
)
latex
Definitions
True
,
T
,
,
t
T
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
x
:
A
.
B
(
x
)
,
S
T
Lemmas
mon
ident
q
,
qinverse
q
,
qadd
comm
q
,
qadd
ac
1
q
,
int
inc
rationals
,
qmul
wf
,
true
wf
,
squash
wf
,
qadd
wf
,
rationals
wf
origin
a, b, c:
. (a = b) 
((c + a) = (c + b) 
) a, b, c:. (a = b) ((c + a) = (c + b) ) 
T
T Q Q Qx:A. B(x)
T